k:, P:(k).
((i:k. P(i))  0<search(k;P))
& (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j))) 

latex

Definitions	AB, A, False, P & Q, P  Q, x:A. B(x), b, , {i..j}, ij, P  Q, x:A. B(x), t  T, , search(k;P), P  Q, Prop, S  T, S  T, i  j < k, x. t(x), Dec(P), P  Q, SQType(T), {T}, i=j, Unit, T, i<j, ij, b, True, if b t else f fi
Lemmas	decidable lt, ifthenelse wf, bnot wf, le int wf, lt int wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, not wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, search wf, decidable assert, decidable ex int seg, le wf, bool wf, int seg wf, assert wf, nat wf, nat properties, ge wf